#ifndef SAT_SOLVER_H
#define SAT_SOLVER_H

#include <def.h>
#include <vec.h>

// forward declaration
namespace Minisat{ struct Lit; };
namespace MinisatProof{ struct Lit; };
namespace CryptoMiniSat{ struct Lit;};


/**
@brief a general literal to support other solver
*/
class Lit
{
   uint32_t x;
   explicit Lit(uint32_t i) : x(i) { };
public:
   explicit Lit(){}
   explicit Lit(uint32_t var, bool sign) : x((var+var) + (int)sign) { }
   bool operator == (Lit p) const { return x == p.x; }
   bool operator != (Lit p) const { return x != p.x; }
   bool operator <  (Lit p) const { return x < p.x;  } // '<' makes p, ~p adjacent in the ordering.
   Lit operator^(uint8_t s)const{return Lit(x^s);}
   Lit operator~()const{return Lit(x^1);}
   uint32_t var()const{return x>>1;}
   uint32_t sign()const{return x&1;}
   operator Minisat::Lit();
   operator CryptoMiniSat::Lit();
   operator MinisatProof::Lit();
};

inline int toDimacs( Lit p) { return p.sign() ? (-(p.var())-1) : (p.var() + 1); } 

const Lit lit_Undef(-1,1);
const Lit lit_Error(-1,0);

// forward declaration 
class SATSolver
{
   public:
   virtual ~SATSolver(){};
   virtual void addClause( vec<Lit> & c )=0;
   inline void addClause( Lit a )
   { 
      static vec<Lit> v(1); 
      v.sz=1,v[0]=a; addClause(v);
   }
   inline void addClause( Lit a , Lit b )
   { 
      static vec<Lit> v(2);
      v.sz=2,v[0]=a,v[1]=b; addClause(v);
   }
   inline void addClause( Lit a , Lit b , Lit c )
   {
      static vec<Lit> v(3);
      v.sz=3,v[0]=a,v[1]=b,v[2]=c; addClause(v);
   }
};

#endif
